STM: deq wf

ABS: eqof(d)

STM: eqof wf

STM: deq property

STM: eqof eq btrue

STM: eqof equal btrue

STM: strong-subtype-deq

STM: strong-subtype-deq-subtype

STM: nat-deq-aux

ABS: NatDeq

STM: nat-deq wf

STM: atom-deq-aux

ABS: AtomDeq

STM: atom-deq wf

STM: atom2-deq-aux

ABS: Atom2Deq

STM: atom2-deq wf

ABS: proddeq(a;b)

STM: proddeq wf

STM: proddeq-property

ABS: prod-deq-aux{v:l,i:l}(A;B;a;b)

STM: prod-deq-aux wf

ABS: prod-deq(A;B;a;b)

STM: prod-deq wf

ABS: product-deq(A;B;a;b)

STM: product-deq wf

ABS: sumdeq(a;b)

STM: sumdeq wf

STM: sumdeq-property

ABS: sum-deq-aux{v:l,i:l}(A;B;a;b)

STM: sum-deq-aux wf

ABS: sum-deq(A;B;a;b)

STM: sum-deq wf

STM: subtype-deq

STM: subtype rel-deq

ABS: union-deq(A;B;a;b)

STM: union-deq wf

ABS: deq-member(eq;x;L)

STM: deq-member wf

STM: assert-deq-member

ABS: DS(A)

STM: discrete struct wf

ABS: dstype(TypeNames; d; a)

STM: dstype wf

STM: decidable dstype equal

ABS: dsdeq(d;a)

STM: dsdeq wf

ABS: dseq(d;a)

STM: dseq wf

ABS: x = y

STM: eq ds wf

STM: ds property

ABS: insert(a;L)

STM: insert wf

STM: insert property

STM: no repeats-insert

STM: member-insert

ABS: l-union(eq;as;bs)

STM: l-union wf

STM: member-union

STM: no repeats union

ABS: l-union-list(eq;ll)

STM: l-union-list wf

STM: member-l-union-list

STM: no repeats-union-list

ABS: remove-repeats(eq;L)

STM: remove-repeats wf

STM: remove-repeats property

STM: member-remove-repeats

ABS: list-diff(eq;as;bs)

STM: list-diff wf

STM: list-diff-property

STM: member-list-diff

ABS: IdDeq

STM: id-deq wf

ABS: a = b

STM: eq id wf

STM: eq id self

STM: assert-eq-id

STM: decidable equal Id

STM: eq id test

ABS: IdLnkDeq

STM: idlnk-deq wf

ABS: a = b

STM: eq lnk wf

STM: assert-eq-lnk

STM: decidable equal IdLnk

STM: lconnects-transitive

STM: decidable l member

ABS: KindDeq

STM: Kind-deq wf

ABS: a = b

STM: eq knd wf

STM: eq knd self

STM: assert-eq-knd

STM: decidable equal Kind

ABS: locl_rcv{locl_rcv_compseq_tag_def:ObjectId}(tg; l; a)

ABS: rcv_locl{rcv_locl_compseq_tag_def:ObjectId}(a; tg; l)

ABS: locl_locl{locl_locl_compseq_tag_def:ObjectId}(b; a)

ABS: rcv rcv compseq tag def

STM: map-concat-filter-lemma1

STM: map-concat-filter-lemma2

ABS: StandardDS

STM: standard-ds wf

ABS: index(L;x)

STM: l index wf

STM: select l index

STM: l before l index

STM: l before l index le

ABS: has-src(i;k)

STM: has-src wf

STM: assert-has-src

ABS: hasloc(k;i)

STM: hasloc wf

STM: assert-hasloc

ABS: kind-loc(k;i)

STM: kind-loc wf

STM: dependent-pair-inherence

STM: no repeats mu index